Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

g(X) → h(X)
c → d
h(d) → g(c)

The replacement map contains the following entries:

g: empty set
h: empty set
c: empty set
d: empty set


↳ CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

g(X) → h(X)
c → d
h(d) → g(c)

The replacement map contains the following entries:

g: empty set
h: empty set
c: empty set
d: empty set

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

g(X) → h(X)
c → d
h(d) → g(c)

The replacement map contains the following entries:

g: empty set
h: empty set
c: empty set
d: empty set

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {g, h, H, G, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

G(X) → H(X)
H(d) → G(c)


The hidden terms of R are:

c

Every hiding context is built from:none

Hence, the new unhiding pairs DPu are :

U(c) → C

The TRS R consists of the following rules:

g(X) → h(X)
c → d
h(d) → g(c)

The set Q consists of the following terms:

g(x0)
c
h(d)


The approximation of the Context-Sensitive Dependency Graph contains 1 SCC.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSUsableRulesProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {g, h, G, H} are not replacing on any position.

The TRS P consists of the following rules:

H(d) → G(c)
G(X) → H(X)

The TRS R consists of the following rules:

g(X) → h(X)
c → d
h(d) → g(c)

The set Q consists of the following terms:

g(x0)
c
h(d)


The following rules are not useable and can be deleted:

g(x0) → h(x0)
c → d
h(d) → g(c)


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSUsableRulesProof
                ↳ QCSDP
                  ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {G, H, g, h} are not replacing on any position.

The TRS P consists of the following rules:

H(d) → G(c)
G(X) → H(X)

R is empty.
The set Q consists of the following terms:

g(x0)
c
h(d)


Using the order
Recursive path order with status [2].
Quasi-Precedence:
d > [H1, G1, c]

Status:
c: multiset
H1: multiset
G1: multiset
d: multiset


the following usable rules
none

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

H(d) → G(c)

could be oriented strictly and thus removed.
The pairs

G(X) → H(X)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSUsableRulesProof
                ↳ QCSDP
                  ↳ QCSDPReductionPairProof
                    ↳ QCSDP
                      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {H, G, g, h} are not replacing on any position.

The TRS P consists of the following rules:

G(X) → H(X)

R is empty.
The set Q consists of the following terms:

g(x0)
c
h(d)


The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.